Conversation
|
What besides SAYNT may depend on the old one? I understand the desire to treat carefully, but I also think it may simplify the merging process significantly if we do hard cut. People that want the old version will need to work with 1.14 and as long as it is clear what features we are loosing, that all seems fine to me. |
|
I can't think of anything that depends on the old one besides SAYNT. Featurewise, I think the only significant omission currently is the automated refinement loop for the approximations. I think that needs some conceptual reworking before implementation, so I have omitted it for now. All in all, I would be fine with completely removing the old implementation. As we are reworking SAYNT, there should be no reason for keeping it. |
|
Would it make sense to split this PR into one that touches storm and one that only touches storm-pomdp? Also, within storm-pomdp, I was wondering whether some parts of the CLI should actually be moved into their own header/cpp (pomdp-handling.h) or so such that it is a bit clearer where it is just cli handling and where it is configuring the algorithm? |
|
I'll split the PR. That definitely makes things more manageable. |
# Conflicts: # src/storm-pomdp/builder/BeliefMdpExplorer.cpp # src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp # src/test/storm-pomdp/api/BeliefExplorationAPITest.cpp # src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp
# Conflicts: # src/storm/logic/BoundedUntilFormula.cpp
tquatmann
left a comment
tquatmann
left a comment
There was a problem hiding this comment.
I haven't finished my review yet but here are my comments so far :)
| * Zero level widths unfold a dimension completely and remove its bound. Positive level widths retain a compact | ||
| * epoch representation and introduce a corresponding level reward model. | ||
| */ | ||
| static ReturnType transform(storm::models::sparse::Model<ValueType> const& model, storm::logic::Formula const& formula, |
There was a problem hiding this comment.
Create a test case for this transformation. Should also work for DTMC/MDP (not just POMDP) right?
| template<typename ValueType> | ||
| RewardBoundUnfolder<ValueType>::ReturnType RewardBoundUnfolder<ValueType>::transform(storm::models::sparse::Model<ValueType> const& model, | ||
| storm::logic::Formula const& formula, UnfoldingOptions const& options) { | ||
| if (formula.isProbabilityOperatorFormula()) { |
There was a problem hiding this comment.
Throw for certain model files? Only DTMC, MDP, POMDP should work.
| // Generated observations must not collide with the original observations retained by initial-state copies. | ||
| ObservationType freshObservation = pomdp.getNrObservations(); | ||
| auto getOrAddObservationIndex = [&observationIndexStorage, &freshObservation](TransitionObservation const& obs) { | ||
| auto [it, inserted] = observationIndexStorage.try_emplace(obs, freshObservation); |
There was a problem hiding this comment.
is try_emplace correct here?
There was a problem hiding this comment.
Yes, I think so. We want to get the entry, which we get via the iterator it and insert a new value if it is not already in the map. What do you think may be a problem here?
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
One or more issues must be addressed before approval.
Get a fresh assessment by requesting another Copilot review.
Review effort: Lite
Findings: 6
Open (9)
Resolved since last review (11)
| if (isRewBndReachProb) { | ||
| stateLabeling.addLabelToState("target", targetState); | ||
| for (auto const& [belId, state] : explorationInformation.exploredBeliefs) { | ||
| if (propertyInformation.targetObservations.contains(explorationInformation.discoveredBeliefs.getBeliefFromId(belId).observation() % | ||
| explorationInformation.nrObservationsInPomdp)) { | ||
| stateLabeling.addLabelToState("target", state); | ||
| } | ||
| } | ||
| for (auto const& belId : frontierBeliefs) { | ||
| if (propertyInformation.targetObservations.contains(explorationInformation.discoveredBeliefs.getBeliefFromId(belId).observation() % | ||
| explorationInformation.nrObservationsInPomdp)) { |
| STORM_LOG_THROW(threshold >= 0, storm::exceptions::NotSupportedException, | ||
| "Lower reward bound in dimension " << formulaDim << " is not satisfiable."); |
| for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { | ||
| for (auto choice : transitionMatrix.getRowGroupIndices(state)) { | ||
| for (auto const& entry : transitionMatrix.getRow(choice)) { | ||
| auto const obs = transitionObservationFunction(state, choice, entry.getColumn()); | ||
| transitionTargetObservations.push_back(obs); |
…t generate terminal beliefs
This PR contains the revised POMDP belief exploration implementation.
The revised implementation is more modular, making it easier to add extensions.
In addition, it is more performant than the old one.
This PR also adds the functionality to analyse reward-bounded reachability properties on POMDP, as described in https://proceedings.mlr.press/v286/bork25a.html
The revised implementation is fully replacing the current one.
Wo do not port over all functionality from the old implementation.
Changes outside of Storm-POMDP are part of separate PR #1028